3.9 Stateflow (MDL) Module

3.9 Stateflow (MDL) Module

Stateflow® is a commercial software of the MathWorks Company. It has been widely used in industry, .e.g, automobile, to specify and simulate embedded control systems. Stateflow enables graphical representation of hierarchical and parallel state machines with flow charts to describe complex logic. The simulation ability of Stateflow alows users to quickly and visually analyze system behavior under particular circustances. Unfortunately, the semantics of Stateflow is informally, and even partially, described in its 1358 page long user's guide [Mat09]. Moreover, checking systems by means of simulation becomes deficient when dealing with 1) high-level assurance which usually requires testing over a large number of circumstances and 2) open systems whose exact input functions are often unkown.

We apply PAT to improve the reliability of Stateflow: execution semantics of Stateflow diagrams is formally modelled by PAT's CSP# specification language, and important requirements such as safety can be expressed as CSP# assertions and be automatically validated in PAT. In this module, i.e., Stateflow (MDL) module, we have developed and embedded a translator to automatically transform Stateflow diagrams, stored textually in MDL files, into CSP# models.